SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Definite assignment analysis</title>

</head>

Definite assignment analysis

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">In <a href="Computer_science" title="Computer science">computer science</a>, definite assignment analysis is a <a href="Data-flow_analysis" title="Data-flow analysis">data-flow analysis</a> used by <a href="Compiler" title="Compiler">compilers</a> to conservatively ensure that a variable or location is always assigned before it is used.

<div class="mw-heading mw-heading2"><h2 id="Motivation">Motivation</h2></div>

In <a href="C_programming_language" class="mw-redirect" title="C programming language">C</a> and <a href="C%2B%2B" title="C++">C++</a> programs, a source of particularly difficult-to-diagnose errors is the nondeterministic behavior that results from reading <a href="Uninitialized_variable" title="Uninitialized variable">uninitialized variables</a>; this behavior can vary between platforms, builds, and even from run to run.

There are two common ways to solve this problem. One is to ensure that all locations are written before they are read. <a href="Rice's_theorem" title="Rice's theorem">Rice's theorem</a> establishes that this problem cannot be solved in general for all programs; however, it is possible to create a conservative (imprecise) analysis that will accept only programs that satisfy this constraint, while rejecting some correct programs, and definite assignment analysis is such an analysis. The <a href="Java_programming_language" class="mw-redirect" title="Java programming language">Java</a><a href="#cite_note-1">[1]</a> and <a href="C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a><a href="#cite_note-2">[2]</a> programming language specifications require that the compiler report a compile-time error if the analysis fails. Both languages require a specific form of the analysis that is spelled out in meticulous detail. In Java, this analysis was formalized by Stärk et al.,<a href="#cite_note-3">[3]</a> and some correct programs are rejected and must be altered to introduce explicit unnecessary assignments. In C#, this analysis was formalized by Fruja, and is precise as well as sound, in the sense that all variables assigned along all control flow paths will be considered definitely assigned.<a href="#cite_note-fruja-4">[4]</a> The <a href="Cyclone_(programming_language)" title="Cyclone (programming language)">Cyclone</a> language also requires programs to pass a definite assignment analysis, but only on variables with pointer types, to ease porting of C programs.<a href="#cite_note-5">[5]</a>

The second way to solve the problem is to automatically initialize all locations to some fixed, predictable value at the point at which they are defined, but this introduces new assignments that may impede performance. In this case, definite assignment analysis enables a <a href="Compiler_optimization" class="mw-redirect" title="Compiler optimization">compiler optimization</a> where redundant assignments — assignments followed only by other assignments with no possible intervening reads — can be eliminated. In this case, no programs are rejected, but programs for which the analysis fails to recognize definite assignment may contain redundant initialization. The <a href="Common_Language_Infrastructure" title="Common Language Infrastructure">Common Language Infrastructure</a> relies on this approach.<a href="#cite_note-6">[6]</a>

<div class="mw-heading mw-heading2"><h2 id="Terminology">Terminology</h2></div>

A variable or location can be said to be in one of three states at any given point in the program:

<ul><li>Definitely assigned: The variable is known with certainty to be assigned.</li>

<li>Definitely unassigned: The variable is known with certainty to be unassigned.</li>

<li>Unknown: The variable may be assigned or unassigned; the analysis is not precise enough to determine which.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="The_analysis">The analysis</h2></div>

The following is based on Fruja's formalization of the C# intraprocedural (single method) definite assignment analysis, which is responsible for ensuring that all local variables are assigned before they are used.<a href="#cite_note-fruja-4">[4]</a> It simultaneously does definite assignment analysis and <a href="Constant_propagation" class="mw-redirect" title="Constant propagation">constant propagation</a> of boolean values. We define five static functions:

<th>Domain</th>

<th>Description

</th></tr>

<tr>

<td>before</td>

<td>All statements and expressions</td>

<td>Variables definitely assigned before the evaluation of the given statement or expression.

</td></tr>

<tr>

<td>after</td>

<td>All statements and expressions</td>

<td>Variables definitely assigned after the evaluation of the given statement or expression, assuming it completes normally.

</td></tr>

<tr>

<td>All statements and expressions</td>

<td>All variables available in the scope of the given statement or expression.

</td></tr>

<tr>

<td>All boolean expressions</td>

<td>Variables definitely assigned after the evaluation of the given expression, assuming the expression evaluates to true.

</td></tr>

<tr>

<td>false</td>

<td>All boolean expressions</td>

<td>Variables definitely assigned after the evaluation of the given expression, assuming the expression evaluates to false.

</td></tr></tbody></table>

We supply data-flow equations that define the values of these functions on various expressions and statements, in terms of the values of the functions on their syntactic subexpressions. Assume for the moment that there are no goto, break, continue, return, or <a href="Exception_handling" title="Exception handling">exception handling</a> statements. Following are a few examples of these equations:

<ul><li>Any expression or statement e that does not affect the set of variables definitely assigned: after(e) = before(e)</li>

<li>Let e be the assignment expression loc = v. Then before(v) = before(e), and after(e) = after(v) U {loc}.</li>

<li>Let e be the expression true. Then true(e) = before(e) and false(e) = vars(e). In other words, if e evaluates to false, all variables are (<a href="Vacuous_truth" title="Vacuous truth">vacuously</a>) definitely assigned, because e does not evaluate to false.</li>

<li>Since method arguments are evaluated left to right, before(argi + 1) = after(argi). After a method completes, out parameters are definitely assigned.</li>

<li>Let s be the conditional statement if (e) s1 else s2. Then before(e) = before(s), before(s1) = true(e), before(s2) = false(e), and after(s) = after(s1) intersect after(s2).</li>

<li>Let s be the while loop statement while (e) s1. Then before(e) = before(s), before(s1) = true(e), and after(s) = false(e).</li>

At the beginning of the method, no local variables are definitely assigned. The verifier repeatedly iterates over the <a href="Abstract_syntax_tree" title="Abstract syntax tree">abstract syntax tree</a> and uses the data-flow equations to migrate information between the sets until a <a href="Fixed_point_(mathematics)" title="Fixed point (mathematics)">fixed point</a> can be reached. Then, the verifier examines the before set of every expression that uses a local variable to ensure that it contains that variable.

The algorithm is complicated by the introduction of control-flow jumps like goto, break, continue, return, and exception handling. Any statement that can be the target of one of these jumps must intersect its before set with the set of definitely assigned variables at the jump source. When these are introduced, the resulting data flow may have multiple fixed points, as in this example:

<div class="mw-highlight mw-highlight-lang-c mw-content-ltr mw-highlight-lines" dir="ltr"><pre> int i = 1;

L:

goto L;

</pre></div>

Since the label L can be reached from two locations, the control-flow equation for goto dictates that before(2) = after(1) intersect before(3). But before(3) = before(2), so before(2) = after(1) intersect before(2). This has two fixed-points for before(2), {i} and the empty set. However, it can be shown that because of the monotonic form of the data-flow equations, there is a unique maximal fixed point (fixed point of largest size) that provides the most possible information about the definitely assigned variables. Such a maximal (or maximum) fixed point may be computed by standard techniques; see <a href="Data-flow_analysis" title="Data-flow analysis">data-flow analysis</a>.

An additional issue is that a control-flow jump may render certain control flows infeasible; for example, in this code fragment the variable i is definitely assigned before it is used:

if (j < 0) return; else i = j;

print(i);

</pre></div>

The data-flow equation for if says that after(2) = after(return) intersect after(i = j). To make this work out correctly, we define after(e) = vars(e) for all control-flow jumps; this is vacuously valid in the same sense that the equation false(true) = vars(e) is valid, because it is not possible for control to reach a point immediately after a control-flow jump.

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFJ._GoslingB._JoyG._SteeleG._Bracha" class="citation web cs1">J. Gosling; B. Joy; G. Steele; G. Bracha. <a rel="nofollow" class="external text" href="http://java.sun.com/docs/books/jls/third_edition/html/defAssign.html">"The Java Language Specification, 3rd Edition"</a>. pp. Chapter 16 (pp.527–552). Retrieved December 2, 2008.</cite>

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.ecma-international.org/publications/standards/Ecma-334.htm">"Standard ECMA-334, C# Language Specification"</a>. ECMA International. pp. Section 12.3 (pp.122–133). Retrieved December 2, 2008.</cite>

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> <cite id="CITEREFStärkE._BorgerJoachim_Schmid2001" class="citation book cs1">Stärk, Robert F.; E. Borger; Joachim Schmid (2001). Java and the Java Virtual Machine: Definition, Verification, Validation. Secaucus, NJ, USA: Springer-Verlag New York, Inc. pp. Section 8.3. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>3-540-42088-6</bdi>.</cite>

</li>

<li id="cite_note-fruja-4">^ <a href="#cite_ref-fruja_4-0">a</a> <a href="#cite_ref-fruja_4-1">b</a> <cite id="CITEREFFruja2004" class="citation journal cs1">Fruja, Nicu G. (October 2004). <a rel="nofollow" class="external text" href="http://www.jot.fm/issues/issue_2004_10/article2">"The Correctness of the Definite Assignment Analysis in C#"</a>. Journal of Object Technology. 3 (9): 29–52. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.6696">10.1.1.165.6696</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.5381%2Fjot.2004.3.9.a2">10.5381/jot.2004.3.9.a2</a>. Retrieved 2008-12-02. <q>We actually prove more than correctness: we show that the solution of the analysis is a perfect solution (and not only a safe approximation).</q></cite>

</li>

<li id="cite_note-5"><a href="#cite_ref-5">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://cyclone.thelanguage.org/wiki/Definite%20Assignment">"Cyclone: Definite Assignment"</a>. Cyclone User's Manual. Retrieved December 16, 2008.</cite>

</li>

<li id="cite_note-6"><a href="#cite_ref-6">^</a> <cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.ecma-international.org/publications/standards/Ecma-335.htm">"Standard ECMA-335, Common Language Infrastructure (CLI)"</a>. ECMA International. pp. Section 1.8.1.1 (Partition III, pg. 19). Retrieved December 2, 2008.</cite>

</li>

</ol></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2020-05-11" href="https://en.wikipedia.org/wiki/?title=Definite_assignment_analysis&oldid=956133309">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>